/LMAR=0/XLINE=3/FONT#0=BAXL30/FONT#1=BAXM30/FONT#2=BASB30/FONT#3=SUB/FONT#4=SUP/FONT#5=BASL35/FONT#6=NGR25/FONT#7=MATH30/FONT#8=FIX25/FONT#9=GRKB30/FONT#10=BDJ20/FONT#10=BDJ20
␈↓ α∧␈↓␈↓ u1


␈↓ α∧␈↓α␈↓ ∧/THE PROGRAMMING LANGUAGE ELEPHANT

␈↓ α∧␈↓␈↓ ελby John McCarthy

␈↓ α∧␈↓␈↓ αTThe␈α⊗Elephant␈α⊗(it␈α⊗never␈α⊗forgets)␈α⊗algorithmic␈α⊗language␈α⊗does␈α⊗assignment␈α↔by␈α⊗regarding
␈↓ α∧␈↓variables␈αas␈αexplicit␈αfunctions␈αof␈αtime;␈αe.g.␈αwhere␈αAlgol␈αexpects␈α␈↓↓x :=␈↓,␈αElephant␈αexpects␈α␈↓↓x(t) =␈↓.␈α The
␈↓ α∧␈↓program␈α⊂counter␈α∂is␈α⊂also␈α∂explicitly␈α⊂regarded␈α∂as␈α⊂a␈α∂function␈α⊂of␈α∂time.␈α⊂ Overcoming␈α⊂the␈α∂inhibition
␈↓ α∧␈↓against␈α∂explicit␈α⊂use␈α∂of␈α⊂time␈α∂as␈α⊂the␈α∂independent␈α∂variable␈α⊂allows␈α∂programs␈α⊂to␈α∂be␈α⊂represented␈α∂as
␈↓ α∧␈↓collections␈α
of␈α
sentences␈αin␈α
a␈α
first␈αorder␈α
logical␈α
language␈α
that␈αcan␈α
be␈α
used␈αto␈α
prove␈α
properties␈αof␈α
the
␈↓ α∧␈↓program.␈α∪ Moreover,␈α∩allowing␈α∪the␈α∩right␈α∪hand␈α∩sides␈α∪of␈α∩equations␈α∪to␈α∩refer␈α∪to␈α∩other␈α∪than␈α∩the
␈↓ α∧␈↓immediate␈αpast␈αallows␈α"high␈αlevel"␈αprograms␈αthat␈αdon't␈αrequire␈αdata␈αstructure␈αdefinitions␈αrequired
␈↓ α∧␈↓by␈α∞ordinary␈α∞programming␈α∞languages.␈α∞ The␈α∞concepts␈α∞are␈α∞best␈α∞understood␈α∞by␈α∞means␈α∞of␈α
examples.
␈↓ α∧␈↓The notation is as in (Cartwright and McCarthy 1979).

␈↓ α∧␈↓1. Translating a sequential program into Elephant

␈↓ α∧␈↓␈↓ αTConsider␈α⊂the␈α⊃following␈α⊂Algol␈α⊃60␈α⊂program␈α⊃fragment␈α⊂(declarations␈α⊃are␈α⊂omitted)␈α⊃for␈α⊂doing
␈↓ α∧␈↓multiplication by addition:

␈↓ α∧␈↓↓␈↓ αTi := n;␈↓ εt0
␈↓ α∧␈↓↓␈↓ αTp := 0;␈↓ εt1
␈↓ α∧␈↓↓loop:   ␈↓αif␈↓↓ i = 0 ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;␈↓ εt2
␈↓ α∧␈↓↓␈↓ αTi := i - 1;␈↓ εt3
␈↓ α∧␈↓↓␈↓ αTp := p + m;␈↓ εt4
␈↓ α∧␈↓↓␈↓ αT␈↓αgo to␈↓↓ loop;␈↓ εt5
␈↓ α∧␈↓↓done:␈↓ εt6

␈↓ α∧␈↓The corresponding Elephant program consists of the equations

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE i(t)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 4 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE p(t)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 2 ∧ i(t) = 0 THEN 6
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 5 THEN 2
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTIn␈α∂these␈α∂equations␈α∂␈↓↓i(t)␈↓␈α∂and␈α∂␈↓↓p(t)␈↓␈α∂replace␈α∞the␈α∂simple␈α∂variables␈α∂of␈α∂the␈α∂Algol␈α∂program.␈α∞ The
␈↓ α∧␈↓function␈α⊃␈↓↓pc(t)␈↓␈α⊂is␈α⊃the␈α⊂program␈α⊃counter,␈α⊂and␈α⊃it␈α⊃takes␈α⊂values␈α⊃from␈α⊂1␈α⊃to␈α⊂6,␈α⊃corresponding␈α⊃to␈α⊂the
␈↓ α∧␈↓numbers␈αwritten␈αon␈α
the␈αright␈αof␈α
the␈αAlgol␈αprogram.␈α
 It␈αshould␈αbe␈α
apparent␈αfrom␈αthe␈αexample␈α
that
␈↓ α∧␈↓any␈αprogram␈αmade␈αup␈αof␈αassignments␈α
and␈α␈↓αgo to␈↓s␈αcan␈αbe␈αsystematically␈αtranslated␈αto␈α
an␈αElephant
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u2


␈↓ α∧␈↓program.␈α We␈αhave␈α
used␈αthe␈αlogical␈α
conditional␈αexpression␈α␈↓↓IF ... THEN ... ELSE␈↓␈α
rather␈αthan
␈↓ α∧␈↓␈↓αif␈↓ ... ␈↓αthen␈↓ ... ␈↓αelse␈↓,␈αbecause␈α
there␈αis␈α
no␈αreason␈α
to␈αprovide␈αfor␈α
an␈αundefined␈α
case.␈α If␈α
the␈αreader␈α
is␈αa
␈↓ α∧␈↓reactionary␈α
and␈α∞doesn't␈α
want␈α
to␈α∞admit␈α
conditional␈α
expressions␈α∞as␈α
terms␈α
in␈α∞first␈α
order␈α∞logic,␈α
then
␈↓ α∧␈↓they can be eliminated.  The equation for ␈↓↓i(t+1)␈↓ would then split into the three cases

␈↓ α∧␈↓↓∀t.[pc(t) = 0 ⊃ i(t+1) = 0 ∧ pc(t) = 1 ⊃ i(t+1) = i(t) - 1
␈↓ α∧␈↓↓␈↓ β∧∧ pc(t) ≠ 0 ∧ pc(t) ≠ 1 ⊃ i(t+1) = i(t)]

␈↓ α∧␈↓␈↓ αTNotice␈α∞also␈α∞that␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Elephant␈α∞program␈α∂is␈α∞linear␈α∞in␈α∂the␈α∞length␈α∞of␈α∂the␈α∞Algol
␈↓ α∧␈↓program.

␈↓ α∧␈↓␈↓ αTHaving␈αone␈α
value␈αof␈α␈↓↓pc(t)␈↓␈α
for␈αeach␈αstatement␈α
in␈αthe␈αAlgol␈α
program␈αis␈αunnecessary,␈α
although
␈↓ α∧␈↓it␈αmakes␈αthe␈αsystematic␈αcharacter␈αof␈αthe␈αtranslation␈αmore␈αapparent.␈α If␈αwe␈αlet␈α␈↓↓pc(t) = 0␈↓␈αcorrespond
␈↓ α∧␈↓to␈α
the␈αinitialization,␈α
␈↓↓pc(t) = 1␈↓␈αcorrespond␈α
to␈α
the␈αloop,␈α
and␈α␈↓↓pc(t) = 2␈↓␈α
correspond␈αto␈α
the␈α
label␈α␈↓↓done,␈↓
␈↓ α∧␈↓then the equations become

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[i(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ β4ELSE i(t)],

␈↓ α∧␈↓↓∀t.[p(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ i(t) ≠ 0 THEN p(t) + m
␈↓ α∧␈↓↓␈↓ β4ELSE p(t)],

␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 ∧ i(t) ≠ 0 THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTThe correctness of the first version of the Elephant program is given by the sentence

␈↓ α∧␈↓␈↓ αT␈↓↓∀m n ∃t.[pc(t) = 6 ∧ p(t) = mn]␈↓,

␈↓ α∧␈↓while␈α∀the␈α∪modified␈α∀program␈α∪would␈α∀have␈α∀the␈α∪same␈α∀correctness␈α∪condition␈α∀except␈α∀for␈α∪having
␈↓ α∧␈↓␈↓↓pc(t) = 2␈↓␈αinstead␈αof␈α␈↓↓pc(t) = 6.␈↓␈αEither␈αstatement␈αis␈αprovable␈αfrom␈αany␈αfirst␈αorder␈αaxiomatization␈αof
␈↓ α∧␈↓arithmetic␈αtogether␈αwith␈αthe␈αsentences␈αconstituting␈αthe␈αprogram.␈α No␈αspecial␈αaxioms␈αfor␈αprograms
␈↓ α∧␈↓or "logic of programs" is required.

␈↓ α∧␈↓␈↓ αTThus␈α
an␈α
entirely␈α
conventional␈α
mathematical␈α
way␈α
of␈α
writing␈α
recursion␈α
equations␈α
leads␈α∞to␈α
a
␈↓ α∧␈↓convenient␈α∂programming␈α∂language.␈α∞ I␈α∂am␈α∂tempted␈α∂to␈α∞call␈α∂the␈α∂language␈α∞Algol␈α∂50,␈α∂since␈α∂it␈α∞could
␈↓ α∧␈↓easily have been developed at that time.

␈↓ α∧␈↓␈↓ αTThe␈α
proof␈α
of␈α
correctness␈α
for␈α
this␈αmultiplication␈α
program␈α
is␈α
misleadingly␈α
simple,␈α
since␈αwe␈α
can
␈↓ α∧␈↓easily␈αwrite␈αexplicit␈αformulas␈αfor␈α␈↓↓i(t),␈↓␈α␈↓↓p(t),␈↓␈αand␈α␈↓↓pc(t)␈↓␈αand␈αprove␈αthem␈αby␈αmathematical␈αinduction.
␈↓ α∧␈↓More␈α
typical␈α
proofs␈α
occur␈α
when␈α
it␈α
isn't␈α
convenient␈α
to␈α
give␈α
explicit␈α
formulas␈α
for␈α
the␈α
variables␈αas
␈↓ α∧␈↓functions␈α
of␈α
time␈α
or␈α
for␈αthe␈α
value␈α
of␈α
␈↓↓t␈↓␈α
for␈αwhich␈α
the␈α
program␈α
terminates.␈α
 Then␈αthe␈α
computational
␈↓ α∧␈↓content␈α⊃of␈α⊃the␈α⊃proof␈α⊃is␈α⊃is␈α⊃often␈α⊃essentially␈α⊃the␈α⊃same␈α⊃as␈α⊃that␈α⊃of␈α⊃an␈α⊃␈↓↓inductive␈α∩assertions␈↓␈α⊃proof
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u3


␈↓ α∧␈↓combined␈α∀with␈α∀induction␈α∀on␈α∀a␈α∀rank␈α∀function␈α∪of␈α∀the␈α∀variables␈α∀taking␈α∀values␈α∀in␈α∀a␈α∪suitable
␈↓ α∧␈↓inductively ordered set.

␈↓ α∧␈↓2. Reversing a list

␈↓ α∧␈↓␈↓ αTReversing␈α
a␈α
list␈α
provides␈α
another␈α
example␈αof␈α
an␈α
Elephant␈α
program␈α
that␈α
can␈α
be␈αcompared
␈↓ α∧␈↓with␈α∂a␈α∂recursive␈α∂conditional␈α∂expression␈α∂program␈α∂for␈α∂the␈α∂same␈α∂function.␈α∂ We␈α∂start␈α∂with␈α⊂a␈α∂Lisp
␈↓ α∧␈↓"program feature" program written in the style of Algol 60.

␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := w;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := ␈↓NIL␈↓↓;
␈↓ α∧␈↓↓␈↓ αTloop:   ␈↓αif␈↓↓ null u ␈↓αthen␈↓↓ ␈↓αgo to␈↓↓ done;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtv := [␈↓αa␈↓↓ u] . v;
␈↓ α∧␈↓↓␈↓ αT␈↓ αtu := ␈↓αd␈↓↓ u;
␈↓ α∧␈↓↓␈↓ αT␈↓ αt␈↓αgo to␈↓↓ loop;
␈↓ α∧␈↓↓␈↓ αTdone:

␈↓ α∧␈↓␈↓ αTThe corresponding Elephant program is

␈↓ α∧␈↓↓pc(0) = 0,

␈↓ α∧␈↓↓∀t.[u(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN w
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αd␈↓↓ u(t)
␈↓ α∧␈↓↓␈↓ β4ELSE u(t)],

␈↓ α∧␈↓↓∀t.[v(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN ␈↓NIL␈↓↓
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 ∧ ¬null u(t) THEN ␈↓αa␈↓↓ u(t) . v(t)
␈↓ α∧␈↓↓␈↓ β4ELSE v(t)]

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 1 ∧ ¬null u(t) THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE pc(t) + 1].

␈↓ α∧␈↓␈↓ αTThis can be compared with the LISP program ␈↓↓reverse␈↓ defined by

␈↓ α∧␈↓␈↓ αT␈↓↓reverse u ← ␈↓αif␈↓↓ ␈↓αn␈↓↓ u ␈↓αthen␈↓↓ ␈↓NIL␈↓↓ ␈↓αelse␈↓↓ reverse ␈↓αd␈↓↓ u * <␈↓αa␈↓↓ u>␈↓.

␈↓ α∧␈↓With␈α∂the␈α∂latter,␈α∂as␈α⊂shown␈α∂in␈α∂(Cartwright␈α∂and␈α∂McCarthy␈α⊂1979),␈α∂it␈α∂is␈α∂convenient␈α∂to␈α⊂prove␈α∂such
␈↓ α∧␈↓properties␈α⊗as␈α∃␈↓↓reverse reverse u = u␈↓␈α⊗and␈α∃␈↓↓reverse[u * v] = reverse v * reverse u␈↓.␈α⊗ The␈α⊗major␈α∃fact
␈↓ α∧␈↓about the Elephant program is expressed by

␈↓ α∧␈↓␈↓ αT␈↓↓∃t.(pc(t) = 2 ∧ v(t) = reverse w)␈↓.

␈↓ α∧␈↓It␈αcan␈αbe␈αproved␈αby␈αproving␈αthat␈α␈↓↓length␈αu(t)␈↓␈αis␈αa␈αdecreasing␈αfunction␈αof␈α␈↓↓t,␈↓␈αi.e.␈αfor␈αany␈α␈↓↓t␈↓␈αsuch␈αthat
␈↓ α∧␈↓␈↓↓pc(t) < 2,␈↓ there is ␈↓↓t' > t␈↓ such that ␈↓↓length u(t') < length t␈↓, and also that

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[reverse w = reverse u(t) * v(t)]␈↓.

␈↓ α∧␈↓This␈α
is␈α
just␈αanother␈α
␈↓↓inductive␈α
assertions␈↓␈α
proof.␈α So␈α
far␈α
it␈α
seems␈αthat␈α
the␈α
most␈αconvenient␈α
technique
␈↓ α∧␈↓for␈αproving␈αfacts␈αabout␈α
Elephant␈αprograms␈αis␈α␈↓↓inductive␈αassertions␈↓,␈α
which␈αis␈αless␈αflexible␈α
than␈αthe
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u4


␈↓ α∧␈↓technique␈αdescribed␈αin␈α(Cartwright␈αand␈αMcCarthy␈α1979)␈αthat␈αuses␈αthe␈α␈↓↓functional␈αequation␈↓␈αand␈α
the
␈↓ α∧␈↓␈↓↓minimization␈α
schema␈↓.␈α This␈α
is␈αbecause␈α
␈↓↓inductive␈α
assertions␈↓␈αprovides␈α
no␈αway␈α
of␈αexpressing␈α
algebraic
␈↓ α∧␈↓relations among functions defined by programs.

␈↓ α∧␈↓␈↓ αTOne␈α
mathematically␈α
straightforward␈α
way␈α
of␈α
defining␈α
functions␈α
by␈α
programs␈α
is␈αthe␈α
following.
␈↓ α∧␈↓We␈α
rewrite␈α
the␈α
above␈α
equations␈α
to␈α
introduce␈α
␈↓↓w␈↓␈α
as␈α
an␈α
explicit␈α
argument␈α
of␈α
the␈α
functions␈α
so␈αthat
␈↓ α∧␈↓they become ␈↓↓u(t,w),␈↓ ␈↓↓v(t,w),␈↓ and pc(t,w).  We then define a relation ␈↓↓reverses(v,w)␈↓ by

␈↓ α∧␈↓␈↓ αT␈↓↓∀v w.(reverses(v,w) ≡ ∃t.(pc(t,w) = 2 ∧ v(t,w) = v))␈↓.

␈↓ α∧␈↓When␈α∂we␈α∂have␈α∞proved␈α∂␈↓↓∀w␈α∂∃!v.reverses(v,w)␈↓,␈α∂first␈α∞order␈α∂logic␈α∂entitles␈α∞us␈α∂to␈α∂replace␈α∂the␈α∞relation
␈↓ α∧␈↓␈↓↓reverses␈↓ by a function.  We can then prove successively that this function satisfies the relations

␈↓ α∧␈↓␈↓ αT␈↓↓reverse ␈↓NIL␈↓↓ = ␈↓NIL␈↓↓␈↓,

␈↓ α∧␈↓␈↓ αT␈↓↓reverse [x . u] = reverse u * <x>␈↓

␈↓ α∧␈↓␈↓ αT␈↓↓reverse reverse u = u␈↓,

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓reverse[u * v] = reverse v * reverese u␈↓,

␈↓ α∧␈↓where the notation is as in (McCarthy and Talcott 1979).

␈↓ α∧␈↓3. Non Algolic Elephant Programs

␈↓ α∧␈↓␈↓ αTWhen␈αwe␈αtranslate␈αan␈αAlgol␈αprogram␈αinto␈αElephant,␈αwe␈αget␈αequations␈αin␈αwhich␈α
the␈α␈↓↓x(t+1)␈↓s
␈↓ α∧␈↓depend␈α
only␈α
on␈α
the␈α
␈↓↓x(t)␈↓s.␈α
 We␈α
will␈α
call␈α
such␈α
a␈α
program␈α
an␈α
␈↓↓immediate␈↓␈α
Elephant␈α
program.␈α
 However,
␈↓ α∧␈↓the␈αrecursion␈αequations␈αwill␈αstill␈αhave␈αguaranteed␈αsolutions␈αif␈αthe␈α␈↓↓x(t)␈↓s␈αdepend␈αon␈αarbitrary␈α
earlier
␈↓ α∧␈↓values of ␈↓↓t.␈↓ This leads to a "high level" programming language with the following features:

␈↓ α∧␈↓␈↓ αT1.␈α∞The␈α
program␈α∞refers␈α∞to␈α
the␈α∞past␈α
through␈α∞earlier␈α∞values␈α
of␈α∞␈↓↓t,␈↓␈α
just␈α∞as␈α∞though␈α
everything
␈↓ α∧␈↓were remembered.  That's why we call the language Elephant.

␈↓ α∧␈↓␈↓ αT2.␈α
The␈αcompiler␈α
is␈α
smart␈αand␈α
decides␈αwhat␈α
data␈α
structures␈αare␈α
required␈α
in␈αorder␈α
to␈αcarry␈α
out
␈↓ α∧␈↓the␈α
computations␈α
without␈α
remembering␈α
everything.␈α∞ To␈α
the␈α
extent␈α
that␈α
compilers␈α
can␈α∞be␈α
written
␈↓ α∧␈↓that␈α
do␈α
this␈α
effectively,␈αElephant␈α
is␈α
a␈α
"higher␈α
level"␈αlanguage␈α
in␈α
which␈α
the␈α
programer␈αspecifies␈α
less
␈↓ α∧␈↓than in Algol, etc.

␈↓ α∧␈↓4. An airline reservation system

␈↓ α∧␈↓␈↓ αTConsider␈α∃programming␈α∃a␈α⊗trivial␈α∃airline␈α∃reservation␈α∃system.␈α⊗ We␈α∃want␈α∃to␈α∃say␈α⊗that␈α∃␈↓↓a
␈↓ α∧␈↓↓passenger␈α∞has␈α
a␈α∞reservation␈α
if␈α∞he␈α
has␈α∞made␈α∞one␈α
that␈α∞has␈α
not␈α∞been␈α
cancelled␈↓.␈α∞ We␈α
do␈α∞not␈α∞want␈α
to
␈↓ α∧␈↓prescribe␈α∂what␈α⊂data␈α∂structures␈α∂have␈α⊂to␈α∂be␈α∂kept␈α⊂in␈α∂order␈α∂to␈α⊂be␈α∂able␈α∂to␈α⊂answer␈α∂the␈α⊂question␈α∂of
␈↓ α∧␈↓whether someone has a reservation.

␈↓ α∧␈↓␈↓ αTThis␈α∀program␈α∀replies␈α∀properly␈α∀to␈α∀requests␈α∀to␈α∀make␈α∀reservations,␈α∀cancel␈α∀them,␈α∀and␈α∪to
␈↓ α∧␈↓inquiries␈α⊂about␈α∂whether␈α⊂a␈α⊂reservation␈α∂exists.␈α⊂ The␈α∂program␈α⊂refers␈α⊂to␈α∂its␈α⊂input␈α∂in␈α⊂terms␈α⊂of␈α∂an
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u5


␈↓ α∧␈↓abstract␈α∀analytic␈α∀syntax␈α∀the␈α∀meaning␈α∀of␈α∀whose␈α∀mnemonic␈α∀predicate␈α∀and␈α∀function␈α∀names␈α∀is
␈↓ α∧␈↓hopefully␈αobvious.␈α The␈αonly␈αdata␈αstructure␈αexplicitly␈αmentioned␈αis␈αthe␈αnumber␈αof␈α
seats␈αcurrently
␈↓ α∧␈↓occupied,␈α
and␈α
even␈α
that␈α
could␈α
be␈αeliminated␈α
from␈α
the␈α
program.␈α
 The␈α
Elephant␈αcompiler,␈α
therefore,
␈↓ α∧␈↓gets␈αthe␈αhonor␈α
of␈αfiguring␈αout␈αwhat␈α
other␈αdata␈αstructures␈αare␈α
needed.␈α We␈αuse␈αthe␈α
convention␈αof
␈↓ α∧␈↓writing ␈↓↓{x}f␈↓ instead of ␈↓↓f(x)␈↓ when it is convenient to write the argument before the function name.

␈↓ α∧␈↓↓␈↓ αT∀t.[output(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You had it"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE IF number(t) = N THEN "No room"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You have it now"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "It's cancelled"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have it to cancel"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF isinquiry in THEN␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN "You have one"
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE "You don't have one"]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE ␈↓NIL␈↓↓]

␈↓ α∧␈↓↓␈↓ αT∀t.[number(t+1) = {input(t)}[λ in.
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀IF ismake in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) ∨ number(t) = N
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$THEN number(t)
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t) + 1]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE IF iscancel in THEN ␈↓ ε~[␈↓ ε$IF hasrev(maker in,t) THEN number(t) - 1
␈↓ α∧␈↓↓␈↓ αT␈↓ ε$ELSE number(t)]
␈↓ α∧␈↓↓␈↓ αT␈↓ β∀ELSE number(t)]

␈↓ α∧␈↓where

␈↓ α∧␈↓␈↓ αT␈↓↓∀t.[hasrev(passenger,t)␈α∂≡␈α∂∃t1.(t1␈α∂<␈α∂t␈α∂∧␈α∂ismake␈α∞input␈α∂t1␈α∂∧␈α∂passenger␈α∂=␈α∂maker␈α∂input␈α∂t1␈α∞∧
␈↓ α∧␈↓↓number(t1) < N) ∧ ¬∃t2.(t1 < t2 < t ∧ iscancel input t2 ∧ maker input t2 = passenger))]␈↓.

␈↓ α∧␈↓␈↓ αTThe␈α⊃main␈α∩difficulty␈α⊃in␈α⊃making␈α∩a␈α⊃compiler␈α∩for␈α⊃Elephant␈α⊃is␈α∩illustrated␈α⊃by␈α∩the␈α⊃predicate
␈↓ α∧␈↓␈↓↓hasrev.␈↓␈α∞The␈α∂compiler␈α∞has␈α∞to␈α∂understand␈α∞that␈α∂it␈α∞must␈α∞remember␈α∂successful␈α∞reservations␈α∂but␈α∞can
␈↓ α∧␈↓forget␈αunsuccessful␈αattempts␈αat␈αmaking␈αa␈αreservation␈αand␈αthat␈αit␈αcan␈αforget␈αreservations␈αthat␈αhave
␈↓ α∧␈↓been␈α
cancelled.␈α Perhaps␈α
␈↓↓hasrev␈↓␈αshould␈α
be␈αwritten␈α
using␈α
primitives␈αthat␈α
refer␈αexplicitly␈α
to␈αthe␈α
most
␈↓ α∧␈↓recent occurrence of an event, which might permit a less intelligent compiler.

␈↓ α∧␈↓5. Elephant program to count vertices in a list structure
␈↓ α∧␈↓****
␈↓ α∧␈↓There seems to be a bug in this program and the ␈↓↓samefringe␈↓ program
␈↓ α∧␈↓that we hope to fix in a subsequent draft.
␈↓ α∧␈↓****

␈↓ α∧␈↓␈↓ αTAnother␈αcontext␈αin␈αwhich␈αit␈αis␈αpossible␈αto␈αavoid␈αspecifying␈αa␈αdata␈αstructure␈αby␈αreferring␈αto
␈↓ α∧␈↓the␈α∞past,␈α∂occurs␈α∞when␈α∂a␈α∞list␈α∂structure␈α∞is␈α∂to␈α∞be␈α∂scanned.␈α∞ The␈α∂simplest␈α∞example␈α∂is␈α∞a␈α∂program␈α∞to
␈↓ α∧␈↓count the vertices in a list structure.

␈↓ α∧␈↓Here␈α␈↓↓a␈↓␈αis␈αthe␈αlist␈αstructure␈αbeing␈αscanned,␈α␈↓↓x␈↓␈αis␈αa␈αrunning␈αvariable␈αfor␈αthe␈αcurrent␈αstructure,␈αand␈α␈↓↓n␈↓
␈↓ α∧␈↓is the current count.

␈↓ α∧␈↓␈↓ αTBecause␈α∩of␈α∩Elephant's␈α∩ability␈α∩to␈α∩refer␈α∩to␈α∩the␈α∩past,␈α∩we␈α∩can␈α∩write␈α∩this␈α∩program␈α∩without
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u6


␈↓ α∧␈↓specifying␈αa␈αstack.␈α It␈αis␈αup␈αto␈αthe␈αcompiler␈αto␈αdecide␈αthat␈αa␈αstack␈αis␈αappropriate␈αfor␈αimplementing
␈↓ α∧␈↓the algorithm.

␈↓ α∧␈↓↓∀t.[x(t+1) ␈↓ βZ= ␈↓ βtIF pc(t) = 0 THEN a
␈↓ α∧␈↓↓␈↓ βtELSE IF pc(t) = 1 THEN
␈↓ α∧␈↓↓␈↓ ∧J[␈↓ ∧TIF [∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
␈↓ α∧␈↓↓␈↓ ¬TTHEN x(t)
␈↓ α∧␈↓↓␈↓ ∧TELSE IF ¬atom x(t) ∧ ¬seen(car x(t),t) then car x(t)
␈↓ α∧␈↓↓␈↓ ∧TELSE cdr x(mostrecent(t,λt1.¬seen(cdr(x(t1)),t)))]
␈↓ α∧␈↓↓␈↓ βtELSE x(t)]

␈↓ α∧␈↓↓∀t.[n(t+1) ␈↓ βZ= ␈↓ βtIF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ βtELSE IF␈↓ ¬∧pc(t) = 1
␈↓ α∧␈↓↓␈↓ ∧s∧␈↓ ¬∧¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
␈↓ α∧␈↓↓␈↓ ¬TTHEN n(t) + 1
␈↓ α∧␈↓↓␈↓ βtELSE n(t)]

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ βZ= ␈↓ βtIF␈↓ ∧4pc(t) = 1
␈↓ α∧␈↓↓␈↓ ∧#∧␈↓ ∧4¬[∀y.seen(y,t) ⊃ atom y ∨ seen(car y,t) ∧ seen(cdr y, t)]
␈↓ α∧␈↓↓␈↓ ¬∧THEN 1
␈↓ α∧␈↓↓␈↓ βtELSE pc(t) + 1

␈↓ α∧␈↓where the predicate ␈↓↓seen␈↓ and the functional ␈↓↓mostrecent␈↓ are defined as follows:

␈↓ α∧␈↓↓∀y t.[seen(y,t) ≡ ∃t1.[t1 ≤ t ∧ y = x(t1)]]

␈↓ α∧␈↓↓∀t.[mostrecent(t, pred) = ␈↓αif␈↓↓ pred t ␈↓αthen␈↓↓ t ␈↓αelse␈↓↓ mostrecent(t - 1, pred)].

␈↓ α∧␈↓We␈α⊂would␈α⊂like␈α∂to␈α⊂regard␈α⊂these␈α⊂as␈α∂definitions␈α⊂not␈α⊂as␈α∂programs.␈α⊂ Indeed␈α⊂the␈α⊂compiled␈α∂program
␈↓ α∧␈↓shouldn't␈αcompile␈α
them␈αdirectly,␈α
but␈αshould␈α
do␈αthe␈α
job␈αanother␈α
way␈αthat␈α
uses␈αtime␈α
and␈αspace␈α
more
␈↓ α∧␈↓efficiently.

␈↓ α∧␈↓Of course, this example is less perspicuous than the lisp program

␈↓ α∧␈↓␈↓↓count x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ 1 ␈↓αelse␈↓↓ count ␈↓αa␈↓↓ x + count ␈↓αd␈↓↓ x␈↓

␈↓ α∧␈↓which␈α
scans␈α
the␈α∞vertices␈α
in␈α
the␈α
same␈α∞order.␈α
 But␈α
then␈α
this␈α∞problem␈α
is␈α
especially␈α∞appropriate␈α
for
␈↓ α∧␈↓recursion and Lisp's built-in stack mechanism.

␈↓ α∧␈↓Most␈αlikely␈α
␈↓↓seen␈↓␈αand␈α
␈↓↓mostrecent␈↓␈αwill␈α
occur␈αin␈αother␈α
algorithms␈αwhere␈α
one␈αdoesn't␈α
want␈αto␈α
look␈αat
␈↓ α∧␈↓things that have been already tried.

␈↓ α∧␈↓6. ␈↓↓samefringe␈↓

␈↓ α∧␈↓␈↓ αTThe LISP predicate ␈↓↓samefringe[x,y]␈↓ may be defined by

␈↓ α∧␈↓␈↓↓samefringe[x1,x2] ≡ fringe x1 = fringe x2␈↓,

␈↓ α∧␈↓where ␈↓↓fringe x␈↓ is a list of the atoms in ␈↓↓x␈↓ and is defined by
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u7


␈↓ α∧␈↓␈↓↓fringe x ← ␈↓αif␈↓↓ ␈↓αa␈↓↓t x ␈↓αthen␈↓↓ <x> ␈↓αelse␈↓↓ fringe ␈↓αa␈↓↓ x . fringe ␈↓αd␈↓↓ x␈↓.

␈↓ α∧␈↓␈↓ αTThe␈αabove␈α
definition␈αdoes␈αnot␈α
provide␈αthe␈α
most␈αefficient␈αcomputation␈α
of␈α␈↓↓samefringe,␈↓␈αand␈α
a
␈↓ α∧␈↓better␈α
LISP␈α
function␈α
is␈α
given␈αin␈α
(Cartwright␈α
and␈α
McCarthy␈α
1979),␈αand␈α
a␈α
proof␈α
of␈α
its␈αcorrectness␈α
is
␈↓ α∧␈↓outlined.  A detailed computer-checked proof is given in (Talcott 1979).

␈↓ α∧␈↓␈↓ αTThe following is an Elephant program for ␈↓↓samefringe␈↓.

␈↓ α∧␈↓↓pc(0) = 0

␈↓ α∧␈↓↓∀t.[x1(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN x1
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 THEN
␈↓ α∧␈↓↓␈↓ ¬*[␈↓ ¬4IF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ε$THEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
␈↓ α∧␈↓↓␈↓ ¬4ELSE x1(t)]
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 2 THEN
␈↓ α∧␈↓↓␈↓ ¬*[␈↓ ¬4IF [∃y.seen1(y,t) ∧ ¬atom y ∧ [¬seen1(car y,t) ∨ ¬seen1(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ε$THEN cdr x1(mostrecent(t,λt1.¬seen1(cdr(x1(t1)),t)))
␈↓ α∧␈↓↓␈↓ ¬4 ELSE IF ¬atom x1(t) THEN car x1(t)
␈↓ α∧␈↓↓␈↓ ¬4 ELSE x1(t)]
␈↓ α∧␈↓↓␈↓ β4 ELSE x1(t)]

␈↓ α∧␈↓↓∀t.[x2(t+1) ␈↓ β~= ␈↓ β4IF pc(t) = 0 THEN x2
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 1 THEN
␈↓ α∧␈↓↓␈↓ ¬*[␈↓ ¬4IF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ε$THEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
␈↓ α∧␈↓↓␈↓ ¬4ELSE x2(t)]
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 2 THEN
␈↓ α∧␈↓↓␈↓ ¬*[␈↓ ¬4IF [∃y.seen2(y,t) ∧ ¬atom y ∧ [¬seen2(car y,t) ∨ ¬seen2(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ε$THEN cdr x2(mostrecent(t,λt1.¬seen2(cdr(x2(t1)),t)))
␈↓ α∧␈↓↓␈↓ ¬4 ELSE IF ¬atom x2(t) THEN car x2(t)
␈↓ α∧␈↓↓␈↓ ¬4 ELSE x2(t)]
␈↓ α∧␈↓↓␈↓ β4 ELSE x2(t)]

␈↓ α∧␈↓↓∀t.[pc(t+1) ␈↓ β~= ␈↓ β4IF (pc(t) = 1 ∨ pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) ∧ x1(t) ≠ x2(t)
␈↓ α∧␈↓↓␈↓ ¬4THEN 4
␈↓ α∧␈↓↓␈↓ β4ELSE IF pc(t) = 2 ∧ atom x1(t) ∧ atom x2(t) THEN 1
␈↓ α∧␈↓↓␈↓ β4ELSE IF␈↓ ¬4pc(t) = 1
␈↓ α∧␈↓↓␈↓ ¬→∧ ␈↓ ¬4∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ¬→∧ ␈↓ ¬4∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ε$THEN 5
␈↓ α∧␈↓↓␈↓ β4ELSE IF␈↓ ¬4pc(t) = 1
␈↓ α∧␈↓↓␈↓ ¬∂∧ [␈↓ ¬4∀y.[seen1(y,t) ⊃ atom y ∨ seen1(car y,t) ∧ seen1(cdr y,t)]
␈↓ α∧␈↓↓␈↓ ¬→∨ ␈↓ ¬4∀y.[seen2(y,t) ⊃ atom y ∨ seen2(car y,t) ∧ seen2(cdr y,t)]]
␈↓ α∧␈↓↓␈↓ ε$THEN 4
␈↓ α∧␈↓↓␈↓ β4 ELSE pc(t) + 1]

␈↓ α∧␈↓↓␈↓where␈↓↓

␈↓ α∧␈↓↓∀y t.[seen1(y,t) ≡ ∃t1.[t1 ≤ t ∧ y = x1(t1)]]
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u8


␈↓ α∧␈↓↓␈↓and␈↓↓

␈↓ α∧␈↓↓∀y t.[seen2(y,t) ≡ ∃t1.[t1 ≤ t ∧ y = x2(t1)]].


␈↓ α∧␈↓␈↓ αTAs␈αThurber␈αmight␈αhave␈αput␈αit,␈αcompared␈αto␈αthe␈αrecursive␈αdefinition,␈αthis␈αis␈αa␈αlittle␈αbig␈αand
␈↓ α∧␈↓pretty␈α
ugly.␈α
 However,␈α
it␈αdoes␈α
have␈α
a␈α
certain␈α
brute␈αforce␈α
straightforward␈α
character,␈α
and␈αit␈α
certainly
␈↓ α∧␈↓leaves to the compiler the task of inventing suitable data structures.

␈↓ α∧␈↓␈↓ αTThe theorem to be proved is

␈↓ α∧␈↓␈↓↓(samefringe(x1,x2) ≡ ∃t.(pc(t) = 5)) ∧ (¬samefringe(x1,x2) ≡ ∃t.(pc(t) = 4))␈↓.

␈↓ α∧␈↓7. Parallel processes for computing a sum of functions

␈↓ α∧␈↓␈↓ αTThe␈αfollowing␈αis␈αan␈αElephant␈αprogram␈αto␈αcompute␈α␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓␈αusing␈α␈↓↓k␈↓␈αprocessors.␈α A␈αmaster
␈↓ α∧␈↓processor␈α∞initializes␈α∞the␈α∞variables␈α
␈↓↓n␈↓␈α∞and␈α∞␈↓↓s␈↓␈α∞and␈α
starts␈α∞the␈α∞␈↓↓k␈↓␈α∞slave␈α
processes␈α∞at␈α∞step␈α∞1.␈α∞ A␈α
process
␈↓ α∧␈↓needs␈αexclusive␈αaccess␈αto␈α␈↓↓n␈↓␈αwhen␈αit␈αis␈α
reading␈αit␈αand␈αincrementing␈αit,␈αand␈αit␈αneeds␈αexclusive␈α
access
␈↓ α∧␈↓to␈α
␈↓↓s␈↓␈αwhen␈α
incrementing␈α
it,␈αand␈α
we␈α
only␈αprovide␈α
for␈αexclusive␈α
access␈α
at␈αthese␈α
times.␈α
 We␈αimagine
␈↓ α∧␈↓that␈αcomputing␈α␈↓↓f(n)␈↓␈αtakes␈α␈↓↓time(n)␈↓␈αunits␈αof␈αtime,␈αand␈αthese␈αoperations␈αare␈αdone␈αin␈αparallel.␈α ␈↓↓pc(t)␈↓␈αis
␈↓ α∧␈↓the␈α
program␈α
counter␈α∞for␈α
the␈α
master␈α∞process,␈α
and␈α
␈↓↓pc(i,t)␈↓␈α∞is␈α
the␈α
program␈α∞counter␈α
of␈α
the␈α∞␈↓↓i␈↓th␈α
slave
␈↓ α∧␈↓process.␈α
 The␈α
updating␈α
of␈α
all␈α
variables␈α
except␈α∞the␈α
␈↓↓pc(i,t)␈↓␈α
works␈α
as␈α
in␈α
Algolic␈α
programs,␈α∞but␈α
the
␈↓ α∧␈↓latter requires a more elaborate description.

␈↓ α∧␈↓↓n(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 1 ∧ n(t) ≤ N THEN n(t) + 1
␈↓ α∧␈↓↓␈↓ β∀ELSE n(t)

␈↓ α∧␈↓↓s(t+1)␈↓ αz= ␈↓ β∀IF pc(t) = 0 THEN 0
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t) = 5 THEN s(t) + m(i,t)
␈↓ α∧␈↓↓␈↓ β∀ELSE s(t)

␈↓ α∧␈↓↓m(i,t+1)␈↓ αz= ␈↓ β∀IF pc(i,t) = 3 ∧ n(t) ≤ N THEN n(t)
␈↓ α∧␈↓↓␈↓ β∀ELSE IF pc(i,t+1) = 4 THEN f(m(i,t))
␈↓ α∧␈↓↓␈↓ β∀ELSE m(i,t)

␈↓ α∧␈↓↓pc(t+1) ␈↓ αz= ␈↓ β∀IF pc(t) = 1 ∧ ∃i.(pc(i,t) ≠ 0) THEN 1
␈↓ α∧␈↓↓␈↓ β∀ELSE pc(t) + 1


␈↓ α∧␈↓↓pc(i,0) = 0

␈↓ α∧␈↓↓pc(i,t) = 0 ⊃ pc(i,t+1) = IF pc(t) = 0 THEN 1 ELSE 0

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ ∃!j.(pc(j,t) = 1 ∧ pc(j,t+1) = 2) ∧ ∃t'.(t < t' ≤ t+k ∧ pc(i,t') = 2)

␈↓ α∧␈↓↓pc(i,t) = 1 ⊃ pc(i,t+1) = 1 ∨ pc(i,t+1) = 2

␈↓ α∧␈↓↓pc(i,t) = 2 ⊃ pc(i,t+1) = IF n(t) ≤ N THEN 3 ELSE 0
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ u9


␈↓ α∧␈↓↓pc(i,t) = 3 ∧ pc(i,t-1) ≠ 3
␈↓ α∧␈↓↓␈↓ β∀⊃ ∀t'.(t ≤ t' < t + time(m(i,t)) ⊃ pc(i,t') = 3) ∧ pc(t+time(m(i,t))) = 4

␈↓ α∧␈↓↓pc(i,t) = 4 ⊃ ∃!j.(pc(j,t) = 4 ∧ pc(j,t+1) = 5) ∧ ∃t'.(t < t' ≤ t + k ∧ pc(i,t') = 5)

␈↓ α∧␈↓↓pc(i,t) = 5 ⊃ pc(i,t+1) = 1

␈↓ α∧␈↓␈↓ αTIt␈α∩may␈α∪be␈α∩questioned␈α∪whether␈α∩the␈α∪above␈α∩Elephant␈α∪program␈α∩should␈α∪be␈α∩regarded␈α∪as␈α∩a
␈↓ α∧␈↓"program"␈α∞that␈α∞can␈α
be␈α∞compiled␈α∞by␈α∞a␈α
suitable␈α∞compiler␈α∞or␈α
as␈α∞something␈α∞between␈α∞a␈α
specification
␈↓ α∧␈↓and␈αa␈α
program.␈α Perhaps␈α
it␈αis␈α
an␈αexample␈α
of␈αthat␈α
elusive␈αconcept␈α
called␈αan␈α
algorithm.␈α Notice␈α
that
␈↓ α∧␈↓it␈α
assumes␈αthat␈α
synchronization␈αoccurs␈α
without␈αspecifying␈α
any␈αway␈α
of␈αdoing␈α
it.␈α Just␈α
the␈α
thing␈αto
␈↓ α∧␈↓challenge␈αa␈αsmart␈αcompiler␈α
or␈αautomatic␈αprogramming␈αsystem.␈α
 On␈αthe␈αother␈αhand,␈αthe␈α
correctness
␈↓ α∧␈↓of the Elephant program is given by the statement,

␈↓ α∧␈↓␈↓↓∃t.(pc(t) = 2 ∧ ∀i(pc(i,t) = 0) ∧ s(t) = ␈↓	S␈↓
␈↓#
N␈↓#␈αp␈↓#vn=1␈↓#␈↓↓f(n))␈↓

␈↓ α∧␈↓and␈α∀this␈α∀can␈α∃presumably␈α∀be␈α∀proved␈α∀from␈α∃the␈α∀program.␈α∀ The␈α∀correspondence␈α∃between␈α∀this
␈↓ α∧␈↓Elephant␈α⊗program␈α∃and␈α⊗one␈α∃that␈α⊗is␈α∃more␈α⊗explicit␈α∃about␈α⊗synchronization␈α∃might␈α⊗be␈α∃proved
␈↓ α∧␈↓separately.

␈↓ α∧␈↓␈↓ αTThere may well be better ways of describing parallel processes in Elephant.

␈↓ α∧␈↓8. Equivalence of Elephant programs.

␈↓ α∧␈↓␈↓ αTDefinitions␈α&of␈α'the␈α&equivalence␈α'of␈α&Elephant␈α'programs,␈α&equivalence-preserving
␈↓ α∧␈↓transformations␈α∩of␈α⊃programs,␈α∩and␈α⊃techniques␈α∩for␈α⊃proving␈α∩equivalence␈α⊃can␈α∩be␈α⊃expected␈α∩to␈α⊃be
␈↓ α∧␈↓important␈α∞in␈α∞applications␈α∞of␈α
Elephant.␈α∞ For␈α∞example,␈α∞one␈α
approach␈α∞to␈α∞compiling␈α∞Elephant␈α∞is␈α
to
␈↓ α∧␈↓transform the program into an immediate program using equivalence-preserving transformations.

␈↓ α∧␈↓␈↓ αTEquivalence␈α
relations␈α
should␈α
be␈α
defined␈α
that␈α
will␈α
facilitate␈α
this␈α
process.␈α
 An␈α
obvious␈αform
␈↓ α∧␈↓of␈α
equivalence␈α
is␈α
to␈α
require␈α
that␈α
each␈α
variable␈α
in␈α
the␈α
two␈α
programs␈α
be␈α
represented␈α
by␈α
the␈α
same
␈↓ α∧␈↓function␈α∪of␈α∪time␈α∪for␈α∩all␈α∪values␈α∪of␈α∪the␈α∩parameters.␈α∪ This␈α∪is␈α∪too␈α∩strict␈α∪an␈α∪equivalence␈α∪to␈α∩be
␈↓ α∧␈↓interesting␈α∂on␈α∂two␈α∂grounds.␈α∞ First,␈α∂the␈α∂two␈α∂forms␈α∂of␈α∞the␈α∂multiplication␈α∂by␈α∂addition␈α∂program␈α∞in
␈↓ α∧␈↓section␈α∞2␈α∞would␈α∞not␈α∞be␈α∞equivalent,␈α∞because␈α∞one␈α∞of␈α∞them␈α∞goes␈α∞around␈α∞the␈α∞loop␈α∞in␈α∞one␈α∞time␈α∞step
␈↓ α∧␈↓while␈αthe␈αother␈αtakes␈αfour␈αsteps.␈α Second,␈αtransforming␈αa␈αprogram␈αto␈αan␈αimmediate␈αprogram␈αmay
␈↓ α∧␈↓involve␈α
the␈αintroduction␈α
of␈αnew␈α
variables,␈α
arrays␈αand␈α
other␈αdata␈α
structures␈αin␈α
order␈α
to␈αeliminate
␈↓ α∧␈↓the direct references to the past.

␈↓ α∧␈↓␈↓ αTWe␈α⊃cannot␈α⊃␈↓↓a␈α⊃priori␈↓␈α⊃exclude␈α⊃the␈α⊂possibility␈α⊃that␈α⊃several␈α⊃concepts␈α⊃of␈α⊃equivalence␈α⊃will␈α⊂be
␈↓ α∧␈↓useful.␈α⊂ However,␈α⊂our␈α⊂first␈α⊃attempt␈α⊂is␈α⊂based␈α⊂on␈α⊂the␈α⊃idea␈α⊂that␈α⊂correspondence␈α⊂of␈α⊃times␈α⊂doesn't
␈↓ α∧␈↓matter␈α⊃so␈α⊂long␈α⊃as␈α⊃the␈α⊂correspondence␈α⊃is␈α⊂monotonic␈α⊃and␈α⊃that␈α⊂we␈α⊃are␈α⊂interested␈α⊃only␈α⊃a␈α⊂certain
␈↓ α∧␈↓correspondence between the states of the program.

␈↓ α∧␈↓␈↓ αTLet␈α∩one␈α∩Elephant␈α∩program␈α∩␈↓↓P␈↓␈α∩have␈α∩functions␈α∩␈↓↓u␈↓#v1␈↓#(t), ... ,u␈↓#vm␈↓#(t)␈↓␈α∩and␈α∩a␈α∩second␈α∩␈↓↓P'␈↓␈α∩have
␈↓ α∧␈↓functions␈α⊂␈↓↓u␈↓#v1␈↓#'(t) ... u␈↓#vn␈↓#'(t).␈↓␈α⊂In␈α⊂order␈α⊂to␈α⊂avoid␈α⊂prolixity,␈α⊂we␈α⊂shall␈α⊂summarize␈α⊂these␈α⊂functions␈α⊂as
␈↓ α∧␈↓vectors␈α
␈↓↓␈↓αu␈↓↓(t)␈↓␈αand␈α
␈↓↓␈↓αu␈↓↓'(t)␈↓.␈α Let␈α
␈↓↓EP(␈↓αu␈↓↓,␈↓αu␈↓↓')␈↓␈αbe␈α
a␈αrelation.␈α
 Let␈αthe␈α
first␈αdepend␈α
on␈αparameters␈α
␈↓↓x␈↓#v1␈↓#, ... x␈↓#vp␈↓#␈↓
␈↓ α∧␈↓and␈α
the␈α
second␈α
have␈α
parameters␈α
␈↓↓x␈↓#v1␈↓#' ... x␈↓#vq␈↓#'␈↓,␈α
similarly␈α
summarized␈α
into␈α
vectors␈α
␈↓↓␈↓αx␈↓↓␈↓␈α
and␈α∞␈↓↓␈↓αx␈↓↓'␈↓.␈α
 (The
␈↓ α∧␈↓parameters␈α∂of␈α∂the␈α∂program␈α∂for␈α∂multiplication␈α∂by␈α∞addition␈α∂were␈α∂␈↓↓m␈↓␈α∂and␈α∂␈↓↓n).␈↓␈α∂Let␈α∂␈↓↓EP(␈↓αx␈↓↓,␈↓αx␈↓↓')␈↓␈α∂be␈α∞a
␈↓ α∧␈↓relation␈αbetween␈αthe␈αparameters.␈α Also␈αlet␈α␈↓↓I(␈↓αx␈↓↓)␈↓␈αand␈α␈↓↓I'(␈↓αx␈↓↓')␈↓␈αbe␈αpredicates␈αthat␈αsay␈αwhat␈αstates␈αof␈α
the
␈↓ α∧␈↓two programs are to be compared.  Now suppose we can prove that
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f10


␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ∧ EP(␈↓αx␈↓↓,␈↓αx␈↓↓') ⊃ EV(␈↓αu␈↓↓(0),␈↓αu␈↓↓'(0)) ∧ I(␈↓αu␈↓↓(0)) ∧ I'(␈↓αu␈↓↓'(0))␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t2 t1'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2 >t1 ∧ I(␈↓αu␈↓↓(t2)) ⊃ ∃t2'.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓

␈↓ α∧␈↓and going the other way

␈↓ α∧␈↓␈↓ αT␈↓↓P ∧ P' ⊃ ∀t1 t1' t2'.[EV(␈↓αu␈↓↓(t1),␈↓αu␈↓↓'(t1')) ∧ t2' >t1' ∧ I'(␈↓αu␈↓↓'(t2')) ⊃ ∃t2.EV(␈↓αu␈↓↓(t2),␈↓αu␈↓↓'(t2'))]␈↓.

␈↓ α∧␈↓We␈α
should␈α
then␈α
call␈α
the␈αprograms␈α
␈↓↓P␈↓␈α
and␈α
␈↓↓P'␈↓␈α
equivalent␈α
with␈αrespect␈α
to␈α
the␈α
the␈α
conditions␈α
␈↓↓I␈↓␈αand␈α
␈↓↓I'␈↓
␈↓ α∧␈↓and␈α∞the␈α∞relations␈α∞␈↓↓EP␈↓␈α∞and␈α∞␈↓↓EV.␈↓␈α∞Note␈α
that␈α∞we␈α∞have␈α∞used␈α∞the␈α∞programs␈α∞themselves␈α∞as␈α
hypotheses
␈↓ α∧␈↓since we can regard a program as the conjunction of its constituent sentences.

␈↓ α∧␈↓␈↓ αTThe two versions of multiplication by addition are equivalent with respect to the predicates

␈↓ α∧␈↓␈↓ αT␈↓↓EP(m,n,m',n') ≡ m=m' ∧ n=n'␈↓

␈↓ α∧␈↓and

␈↓ α∧␈↓␈↓ αT␈↓↓EV(i,p,pc,i',p',pc') ≡ (pc=0 ∧ pc'=0) ∨ [i=i' ∧ p=p' ∧ (pc=2 ∧ pc'=1 ∨ pc=6 ∧ pc'=2)]␈↓

␈↓ α∧␈↓They␈α∞should␈α∞be␈α∞sufficient␈α∞to␈α∞prove␈α∞that␈α∞one␈α∞program␈α∞is␈α∞correct␈α∞(according␈α∞to␈α∞the␈α∞definitlons␈α
of
␈↓ α∧␈↓section␈α2)␈αif␈αand␈αonly␈αif␈αthe␈αother␈αis.␈α We␈αexpect␈αto␈αgive␈αless␈αtrivial␈αexamples␈αof␈αequivalence␈αand
␈↓ α∧␈↓maybe a proof of equivalence in the final version of this paper.

␈↓ α∧␈↓There is some reason to hope that this kind of equivalence will suffice for many applications.

␈↓ α∧␈↓9. Remarks

␈↓ α∧␈↓1.␈α
Programs␈αin␈α
Lucid␈α(Ashcroft␈α
1974)␈αare␈α
also␈α
collections␈αof␈α
sentences␈αin␈α
a␈αfirst␈α
order␈αlanguage.␈α
 A
␈↓ α∧␈↓Lucid␈α∪object␈α∪is␈α∪a␈α∪vector␈α∪of␈α∪the␈α∪values␈α∪of␈α∪a␈α∪variable␈α∪throughout␈α∪time.␈α∪ This␈α∀permits␈α∪some
␈↓ α∧␈↓statements␈α
to␈αbe␈α
made␈αin␈α
a␈αvery␈α
neat␈αway.␈α
 However,␈α
it␈αseems␈α
to␈αbe␈α
less␈αflexible␈α
than␈αthe␈α
Elephant
␈↓ α∧␈↓device␈αof␈αadmitting␈αthe␈αtime␈αas␈αan␈αexplicit␈αparameter.␈α Lucid␈αprograms␈αdo␈αnot␈αadmit␈α␈↓αgo to␈↓s,␈αand
␈↓ α∧␈↓there␈α∂are␈α∂other␈α∂unexpected␈α∂restrictions.␈α∂ Perhaps␈α∂some␈α∂of␈α∂Lucid's␈α∂problems␈α∂would␈α∂be␈α∂cured␈α∞by
␈↓ α∧␈↓admitting a variable playing the role of the program counter.

␈↓ α∧␈↓2.␈αThe␈αproperties␈αof␈αElephant␈αprograms␈αdon't␈αdepend␈αon␈αtime␈αtaking␈αinteger␈αvalues.␈α All␈αwe␈αneed
␈↓ α∧␈↓require␈αis␈αthat␈αthe␈αset␈αof␈αtimes␈αbe␈αordered␈αand␈αunbounded␈αabove.␈α Then␈αthe␈αfirst␈αsentence␈αof␈αthe
␈↓ α∧␈↓product program would take the form

␈↓ α∧␈↓␈↓↓∀t ∃t'.[t' > t ∧ i(t') ␈↓ ∧~= ␈↓ ∧4IF pc(t) = 0 THEN n
␈↓ α∧␈↓↓␈↓ ∧4ELSE IF pc(t) = 3 THEN i(t) - 1
␈↓ α∧␈↓↓␈↓ ∧4ELSE i(t)].

␈↓ α∧␈↓3.␈α∂It␈α∞seems␈α∂to␈α∂me␈α∞that␈α∂any␈α∂language␈α∞that␈α∂purports␈α∞to␈α∂allow␈α∂the␈α∞user␈α∂to␈α∂say␈α∞what␈α∂he␈α∂wants␈α∞the
␈↓ α∧␈↓computer␈αto␈α
do␈αin␈α
English,␈αshould␈α
allow␈αthe␈α
executive␈αor␈αgeneral␈α
or␈αother␈α
big␈αshot␈α
to␈αsay␈α
that␈α␈↓↓a
␈↓ α∧␈↓↓customer␈αhas␈αa␈αreservation␈αif␈αhe␈αhas␈αmade␈αone␈αand␈αit␈αhasn't␈αbeen␈αcancelled␈↓.␈α The␈αbig␈αshot␈αcertainly
␈↓ α∧␈↓doesn't␈α⊂want␈α⊂to␈α∂concern␈α⊂himself␈α⊂with␈α⊂what␈α∂data␈α⊂structures␈α⊂are␈α⊂required␈α∂in␈α⊂order␈α⊂to␈α⊂fulfill␈α∂his
␈↓ α∧␈↓␈↓ ε~incomplete draft␈↓ f11


␈↓ α∧␈↓wishes,␈α∩and␈α∪Elephant␈α∩shows␈α∩that␈α∪his␈α∩wishes␈α∩can␈α∪be␈α∩stated␈α∩without␈α∪mentioning␈α∩such␈α∪a␈α∩data
␈↓ α∧␈↓structure.

␈↓ α∧␈↓4.␈α∂In␈α∂its␈α∂present␈α∂state,␈α∂Elephant␈α∞doesn't␈α∂seem␈α∂to␈α∂be␈α∂a␈α∂very␈α∞easy␈α∂language␈α∂to␈α∂use.␈α∂ I␈α∂say␈α∞"seem",
␈↓ α∧␈↓because␈αthe␈αawkward␈αprograms␈αmay␈αbe␈αmerely␈αa␈αconsequence␈αof␈αinexperience.␈α Of␈αcourse,␈αAlgolic
␈↓ α∧␈↓programs are easy enough to write in Elephant.

␈↓ α∧␈↓5.␈α∞Regarded␈α
simply␈α∞as␈α∞a␈α
way␈α∞of␈α
writing␈α∞Algolic␈α∞programs␈α
as␈α∞logical␈α
sentences,␈α∞Elephant␈α∞plays␈α
a
␈↓ α∧␈↓role␈α⊃similar␈α⊂to␈α⊃that␈α⊃played␈α⊂by␈α⊃the␈α⊃Cartwright␈α⊂way␈α⊃of␈α⊃writing␈α⊂Lisp␈α⊃style␈α⊃recursive␈α⊂conditional
␈↓ α∧␈↓expression␈α∂programs␈α∂as␈α⊂logical␈α∂sentences.␈α∂ In␈α⊂fact␈α∂it␈α∂may␈α⊂be␈α∂a␈α∂kind␈α⊂of␈α∂dual␈α∂to␈α⊂the␈α∂Cartwright
␈↓ α∧␈↓method␈α∂just␈α∂as␈α∂␈↓↓inductive␈α∞assertions␈↓␈α∂and␈α∂␈↓↓subgoal␈α∂induction␈↓␈α∞seem␈α∂to␈α∂be␈α∂duals.␈α∂ Namely,␈α∞Elephant
␈↓ α∧␈↓programs␈αand␈αinductive␈αassertions␈αwork␈αfrom␈αan␈αinitial␈αstate␈αand␈αdescribe␈αits␈αchanges,␈αwhile␈αLisp
␈↓ α∧␈↓style␈α∂programs␈α∂and␈α∂subgoal␈α∂induction␈α∂work␈α∂backwards␈α∂from␈α∂desired␈α∂final␈α∂result.␈α∂ Thus␈α∂it␈α∂may
␈↓ α∧␈↓complete a pattern of methods of program formalization.

␈↓ α∧␈↓6.␈α∞Elephant␈α∞may␈α∞be␈α∞expanded␈α∞by␈α∞relaxing␈α∞the␈α∞restriction␈α∞that␈α∞statements␈α∞refer␈α∞only␈α∞to␈α∞the␈α
past.
␈↓ α∧␈↓Our␈α⊂big␈α⊂shot␈α∂may␈α⊂wish␈α⊂to␈α∂say,␈α⊂␈↓↓"When␈α⊂the␈α⊂passengers␈α∂arrive␈α⊂at␈α⊂the␈α∂airport␈α⊂for␈α⊂the␈α⊂flight,␈α∂an
␈↓ α∧␈↓↓airplane␈α⊃and␈α⊂a␈α⊃crew␈α⊃will␈α⊂have␈α⊃been␈α⊃summoned␈α⊂by␈α⊃the␈α⊂scheduling␈α⊃program␈α⊃to␈α⊂fly␈α⊃them␈α⊃to␈α⊂their
␈↓ α∧␈↓↓destingation"␈↓.␈α Allowing␈α
the␈αright␈α
hand␈αsides␈α
of␈αElephant␈α
equations␈αto␈α
refer␈αto␈α
the␈αfuture␈α
puts␈αa
␈↓ α∧␈↓heavier␈αburden␈αon␈αthe␈αcompiler.␈α In␈αfact,␈αa␈αfuturistic␈αElephant␈αprogram␈αmay␈αbe␈αcontradictory␈α
and
␈↓ α∧␈↓hence␈α
uncompilable.␈α Thus␈α
a␈αcompiler␈α
for␈α
futuristic␈αElephant␈α
is␈αreally␈α
a␈αkind␈α
of␈α
problem␈αsolver.
␈↓ α∧␈↓Only␈α⊃the␈α⊃future␈α⊃can␈α⊃tell␈α⊂if␈α⊃this␈α⊃style␈α⊃of␈α⊃programming␈α⊂will␈α⊃prove␈α⊃useful␈α⊃or␈α⊃even␈α⊂theoretically
␈↓ α∧␈↓illuminating.

␈↓ α∧␈↓7.␈αThe␈αtwo␈αaspects␈αof␈α
Elephant,␈αexplicit␈αuse␈αof␈αthe␈αtime␈α
and␈αprogram␈αcounter␈αand␈αreference␈αto␈α
the
␈↓ α∧␈↓past,␈α∂may␈α∂be␈α∂separated.␈α∂ The␈α∂first␈α∂all␈α∞by␈α∂itself␈α∂provides␈α∂the␈α∂proper␈α∂formalization␈α∂of␈α∞sequential
␈↓ α∧␈↓programs,␈α
and␈α∞there␈α
are␈α∞probably␈α
other␈α∞ways␈α
of␈α
referring␈α∞to␈α
the␈α∞past␈α
than␈α∞by␈α
using␈α∞an␈α
explicit
␈↓ α∧␈↓time␈α⊃variable,␈α⊃e.g.␈α⊃modal␈α⊃tense␈α⊃operators␈α⊃might␈α∩be␈α⊃used.␈α⊃ One␈α⊃of␈α⊃these␈α⊃ways␈α⊃might␈α∩be␈α⊃more
␈↓ α∧␈↓convenient.

␈↓ α∧␈↓10. References

␈↓ α∧␈↓␈↓αCartwright,␈α⊃Robert␈α⊂and␈α⊃John␈α⊂McCarthy␈α⊃(1979)␈↓:␈α⊃"Recursive␈α⊂Programs␈α⊃as␈α⊂Functions␈α⊃in␈α⊃a␈α⊂First
␈↓ α∧␈↓Order Theory", in ␈↓↓


␈↓ α∧␈↓↓This partial draft of ELEPHA[S79,JMC] compiled at 14:15 on May 10, 1979.